| Definitions | e c e', x:A  B(x),  x:A. B(x), case b of inl(x) => s(x) | inr(y) => t(y), P   Q, if b then t else f fi ,  b, s = t, a < b, (x  l), left + right, P  Q, {x:A| B(x)} , E(X), ES, Type, AbsInterface(A),  , Top, e  X, X(e), f(a),  A, E, cr-explanation{i:l}(es; Sys; f; e), effective(e), t T, x:A  B(x), (e < e'), let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B),  , True,  T, Dec(P),  x:A. B(x), e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), SqStable(P), P & Q, P  Q, a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a b, IsIntegDom(r), IsPrimeIdeal(R;P), f  g, sys-antecedent(es;Sys), e loc e' , (e <loc e'), e(e1,e2].P(e), @e(x v), (last change to x before e), A c B, pred(e), Id, P Q, lastchange(x;e), es-init(es;e), f**(e), sender(e), consistent-updates(es;In;Out;Cmd;isupdate;expl), EState(T),  , EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, e < e', constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'),   x,y. t(x;y), !Void(),  x:A.B(x), S T, suptype(S; T), first(e), <a, b>, pred(e), x.A(x), x. t(x), False, ff, inr x , tt, inl x , y is f*(x),  , Outcome, #$n, A B, ||as||, l[i], |g|, [], x dom(f), updates(L), l1 l2, {T}, n+m, n - m, i  j , -n, b | a, a ~ b, a b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), r < s, q-rel(r;x), l_disjoint(T;l1;l2), f(x)?z, es-prior-fixedpoints{i:l}(es; Sys; f; e), [car / cdr], hd(l), last(L), prior(X), y=f*(x) via L, loc(e), es-vartype(es; i; x), es-state(es; i), decl-state(ds), ma-state(ds), s ~ t, b, filter(P;l), as @ bs, SQType(T), p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p q, p q, p q, A List |
| Lemmas | es-le weakening eq, es-fix property, fun-connected transitivity, es-causle weakening locl, es-fix-causl, es-fix wf, strong-subtype-set3, strong-subtype wf, strong-subtype-self, es-fix wf2, nil iseg, subtype rel list, append-nil, filter append, not functionality wrt iff, assert-es-eq-E-2, es-eq-E wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, append wf, filter wf, bnot wf, es-prior-interface-locl, squash wf, fun-connected weakening eq, fun-path wf, es-prior-interface-causl, es-prior-interface wf, iseg-subtype, es-E-interfaces-strong-subtype, length wf1, es-prior-fixedpoints wf, l member subtype, updates of wf, es-interface-subtype rel, filter iseg, decidable assert, es-interface-val wf, decidable es-E-equal, ge wf, nat properties, es-causl-swellfnd, nat ind tp, iseg wf, guard wf, le wf, consistent-updates wf, fun-connected wf, cr-effective wf, length wf nat, select wf, l member wf, cr-explanation wf, es-interface-val wf2, true wf, false wf, btrue wf, bfalse wf, es-interface wf, es-is-interface wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, rationals wf, EState wf, event system wf, es-prior-fixedpoints-iseg, es-le-causle, sys-antecedent wf, es-causle-le, Id wf, es-locl wf, es-le wf, sq stable from decidable, decidable es-causle, es-causl wf, es-causle wf, member wf, es-E wf, es-E-interface wf, subtype rel wf, es-E-interface-subtype rel |
